es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))
== (e:E. kind(e) = rcv(l,tg)  valtype(e)  B) & (x:Id. vartype(source(l);x)  ds(x)?Top)
== & e@source(l). P(e)  (e':E. kind(e') = rcv(l,tg) & sender(e') = e)
== & & (e':E. kind(e') = rcv(l,tg)  P(sender(e')) & val(e') = f(sender(e')))
== & & (e':E.
== & & (kind(e') = rcv(l,tg)
== & & ( (e'':E. isrcv(e'')  lnk(e'') = l  sender(e'') = sender(e')  e'' = e')) 

latex

---

clarification:

es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))
== (e:es-E(es). es-kind(es; e) = rcv(l,tg)  Knd  es-valtype(es; e)  B)
== & (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.P(e)
== & alle-at(es;source(l);e. (e':es-E(es).
== & alle-at(es;source(l);e. (es-kind(es; e') = rcv(l,tg)  Knd
== & alle-at(es;source(l);e. (& es-sender(es; e') = e  es-E(es)))
== & & (e':es-E(es).
== & & (es-kind(es; e') = rcv(l,tg)  Knd
== & & ( P(es-sender(es; e')) & es-val(es; e') = f(es-sender(es; e'))  B)
== & & (e':es-E(es).
== & & (es-kind(es; e') = rcv(l,tg)  Knd
== & & ( (e'':es-E(es).
== & & ( (es-isrcv(es; e'')
== & & ( ( es-lnk(es; e'') = l  IdLnk
== & & ( ( es-sender(es; e'') = es-sender(es; e')  es-E(es)
== & & ( ( e'' = e'  es-E(es))) 

latex

Definitions	valtype(e), Id, vartype(i;x), f(x)?z, IdDeq, Top, e@i. P(e), source(l), x:A. B(x), P & Q, A & B, val(e), Knd, kind(e), rcv(l,tg), x:A. B(x), b, isrcv(e), IdLnk, lnk(e), P  Q, sender(e), s = t, E
FDL editor aliases	es-sends-iff2